<div id = "topbar">
  <img src="assets/icons/3.png">
  <nav>
  <ul>
    <li>
      <span class="topbarMenu btn-success fileinput-button">
        <span>upload folder</span>
        <input type="file" ng2FileSelect [uploader]="uploader" (change)="selectedXMLFileOnChanged($event)"  webkitdirectory mozdirectory >
      </span>
    </li>	
    <li class="topbarMenu" id="OpenProject" (click) = "openProject()">Open</li>
    <li *ngIf="step === 6" class="topbarMenu" id="AddConstraint" (click) = "showConstraintDialog()">Add Constraint</li>
    <li *ngIf="step !== 6" class="cannotTopbarMenu" id="CannotAddConstraint" disabled="disabled">Add Constraint</li>
    <li *ngIf="step >= 6" class="topbarMenu" id="Save" (click) = "saveConstraintsTxt()">Save</li>
    <li *ngIf="6 > step" class="cannotTopbarMenu" id="CannotSave"  disabled="disabled">Save</li>
    <li *ngIf="step >= 7" class="topbarMenu" id="DownloadConstraints" (click) = "downloadConstraints()">DownloadCons</li>
    <li *ngIf="7 > step" class="cannotTopbarMenu" id="CannotDownloadConstraints"  disabled="disabled">DownloadCons</li>
    <li *ngIf="step === 8" class="topbarMenu" id="SemanticCheck" (click) = "showZ3Panel()">Semantics Check</li>
    <li *ngIf="step !== 8" class="cannotTopbarMenu" id="CannotSemanticCheck"  disabled="disabled">Semantics Check</li>
    <li class="topbarMenu" id="help"></li>	
    <!-- <div *ngIf="step >= 8" id="z3Result">waiting......</div>	 -->
  </ul>
  </nav>
</div> 

<div id = "drawingboard">
  <div class="tab">
    <div id="details1DIV" hidden = "hidden">
      <details id="details1" (click) = details1Click() class="details">
        <summary>Sub Clock Diagram</summary>
        <ng-container *ngFor="let diagram of diagrams;let i = index">
            <p *ngIf="diagramCount > i" id = "lm{{i + 1}}" (click) = "change_Menu(i + 1)">{{diagram.title}} : {{diagram.machineName}}</p>
        </ng-container>
      </details>
    </div>

    <div id="details2DIV" hidden = "hidden">
        <details id="details2" (click) = details2Click() class="details">
          <summary>Domain Clock Specification</summary>
          <ng-container *ngFor="let str of domainClockSpecification;let i = index">
              <p (click) = "showDomainClockSpecification(str)">DCS{{(+str.split(',')[0]) + 1}} : {{str.split(',')[1]}}</p>
          </ng-container>
        </details>
      </div>

    <div id="details3DIV" hidden = "hidden">
      <details id="details3" (click) = details3Click() class="details">
          <summary>Timing Diagram</summary>
          <ng-container *ngFor="let diagram of diagrams;let i = index">
              <p *ngIf="i >= diagramCount" id = "lm{{i + 1}}" (click) = "change_Menu(i + 1)">{{diagram.title}} : {{diagram.machineName}}</p>
          </ng-container>
      </details>
    </div>
  </div>
  
	<div class="content" id="content1"></div>
</div>

<div id="rightbar">
    <ul>
      <li class="title">&nbsp;Process of Getting Time Constraints
        <div class="content">
          <ul class="content" *ngIf="step === 0">
            <li style="background:#CFD8DC">&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>	
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step === 1">
            <li>&nbsp;Start</li>
            <li style="background:#CFD8DC">&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>	
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step === 2">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li style="background:#CFD8DC">&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step === 3">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li style="background:#CFD8DC">&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>
            <li>&nbsp;Step 5:Rule Based Checking</li>	
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>

          <ul class="content" *ngIf="step === 4">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li style="background:#CFD8DC">&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step === 5">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li style="background:#CFD8DC">&nbsp;Step 5:Rule Based Checking	</li>
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step === 6">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>
            <li style="background:#CFD8DC">&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step === 7">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li style="background:#CFD8DC">&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step === 8">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li style="background:#CFD8DC">&nbsp;Step 8:Performing Semantics Check</li>	
            <li>&nbsp;Finish</li>
          </ul>
          <ul class="content" *ngIf="step > 8">
            <li>&nbsp;Start</li>
            <li>&nbsp;Step 1:Read the Project File</li>
            <li>&nbsp;Step 2:generate Domain Clock Specification</li>	
            <li>&nbsp;Step 3:generate Timing Diagrams</li>	
            <li>&nbsp;Step 4:Read the Ontology File</li>	
            <li>&nbsp;Step 5:Rule Based Checking</li>	
            <li>&nbsp;Step 6:Manually Add Constraints</li>
            <li>&nbsp;Step 7:Export Timing Constraints</li>
            <li>&nbsp;Step 8:Performing Semantics Check</li>		
            <li style="background:#CFD8DC">&nbsp;Finish</li>
          </ul>
        </div>
      </li><br>
      <button (click) = "previous()">PREVIOUS</button>
      <button (click) = "next()">NEXT</button>
      <div id = "OtherConstraintDIV" hidden = "hidden">
        <li *ngIf="!open1;else elseOpen1" (click)="setOpen1()" class="title">&nbsp;+  Added Constraints</li>
        <ng-template #elseOpen1>
          <li (click)="setOpen1()" class="title">&nbsp;-  Added Constraints</li>
          <div class="content" id = "OtherConstraint" >
            <table *ngFor="let constraint of constraints;let i = index" class="content" id = "consAndBut{{i}}">
              <span id = "cons{{i}}">{{constraint}}</span>
              <button class="DeleteButton" (click)=deleteConstraint(i)>delete</button>
            </table>
          </div>
        </ng-template>
      </div>
      <li *ngIf="!open2;else elseOpen2" (click)="setOpen2()" class="title">&nbsp;+  Phenomenon</li>
      <ng-template #elseOpen2>
        <li (click)="setOpen2()" class="title">&nbsp;-  Phenomenon</li>
        <div class="content">
          <table *ngIf="open2" class="content">
            <tr>
              <th>Name</th>
              <th>Description</th>
              <th>PheType</th>
            </tr>
            <tr *ngFor="let phenomonon of allPhenomena">
              <th>phe {{phenomonon.biaohao}}</th>
              <th>{{phenomonon.name}}</th>
              <th>{{phenomonon.state}}</th>
            </tr>
          </table>	
        </div>
      </ng-template>
      <li *ngIf="!open3;else elseOpen3" (click)="setOpen3()" class="title">&nbsp;+  Interaction</li>
      <ng-template #elseOpen3>
        <li (click)="setOpen3()" class="title">&nbsp;-  Interaction</li>
        <div class="content">
          <table *ngIf="open3" class="content">
            <tr>
              <th>Name</th>
              <th>Initiator</th>
              <th>Receiver</th>
              <th>Content</th>
            </tr>
            <tr *ngFor="let phenomonon of allPhenomena">
              <th>int {{phenomonon.biaohao}}</th>
              <th>{{phenomonon.from.shortName}}</th>
              <th>{{phenomonon.to.shortName}}</th>
              <th>{{phenomonon.name}}</th>
            </tr>
          </table>
        </div>
      </ng-template>
      <li *ngIf="!open4;else elseOpen4" (click)="setOpen4()" class="title">&nbsp;+  Reference</li>
      <ng-template #elseOpen4>
        <li (click)="setOpen4()" class="title">&nbsp;-  Reference</li>
        <div class="content">
          <table *ngIf="open4" class="content">
            <tr>
              <th>Name</th>
              <th>Initiator</th>
              <th>Receiver</th>
              <th>Content</th>
              <th>RefType</th>
            </tr>
            <tr *ngFor="let reference of references">
              <th>req {{reference.requirement.biaohao}}</th>
              <th>{{reference.from.shortName}}</th>
              <th>{{reference.to.shortName}}</th>
              <th>{{reference.name}}</th>
              <th *ngIf="reference.constraining === true">constraining</th>
              <th *ngIf="reference.constraining === false">normal</th>
            </tr>						
          </table>
        </div>
      </ng-template>
      <li *ngIf="!open5;else elseOpen5" (click)="setOpen5()" class="title">&nbsp;+  PD Information</li>
      <ng-template #elseOpen5>
        <li (click)="setOpen5()" class="title">&nbsp;-  PD Information</li>
        <div class="content">
          <table *ngIf="open5" class="content">Information</table>
        </div>
      </ng-template>		
    </ul>
  </div>

  <div id = "z3check">
    <form>
      Timeout:<input type="text" id="timeout" />
      <br/>
      Bound:<input type="text" id="bound" />
      <br/>
      Period:<input type="checkbox" id="hasPeriod" /><input type="text" id="period" />
      <br/>
      Deadlock:<input type="checkbox" id="hasDeadlock" />
      <br/>
      <input type="submit" value="Submit" (click) = "getZ3Result()">
      <input type="submit" value="Cancel" (click) = "goBack()">
    </form>
  </div>


  <div id = "addConstraint">
    <form>
      <select id="from" name = "from" [(ngModel)]="fromInt">
        <option *ngFor="let interaction of interactionsToAdd" value="{{interaction.number}},{{interaction.state}}">int{{interaction.number}},state:{{interaction.state}}</option>
      </select>
      <select name = "cons" [(ngModel)]="cons">
        <option value="StrictPre">StrictPre</option>
        <option value="BoundedDiff">BoundedDiff</option>
        <option value="Cause">Cause</option>
        <option value="Union">Union</option>
        <option value="Alternate">Alternate</option>
        <option value="Delay">Delay</option>
        <option value="Inf">Inf</option>
        <option value="Sup">Sup</option>
        <option value="Exclusion">Exclusion</option>
        <option value="Coincidence">Coincidence</option>
      </select>
      <select id="to" name = "to" [(ngModel)]="toInt">
        <option *ngFor="let interaction of interactionsToAdd" value="{{interaction.number}},{{interaction.state}}">int{{interaction.number}},state:{{interaction.state}}</option>
        <option *ngIf="cons === 'Delay'" value="idealClcok">idealClock</option>
      </select>
      <br>
      <input type="text" *ngIf="cons === 'BoundedDiff'" class="ExtraInput" name="boundedFrom" value="BoundedDiffFrom" [(ngModel)]="boundedFrom">
      <br>
      <input type="text" *ngIf="cons == 'BoundedDiff'" class="ExtraInput" name="boundedTo"  value="BoundedDiffTo" [(ngModel)]="boundedTo">
      <input type="text" *ngIf="cons == 'Union' || cons == 'Inf' || cons == 'Sup'" class="ExtraInput" name="addedClockName" placeholder = "name" value="addedClockName" [(ngModel)]="addedClockName">
      <input type="text" *ngIf="cons == 'Delay'" class="ExtraInput" name="addedTime" placeholder = "time" value="addedTime" [(ngModel)]="addedTime">
      <br><br><br><br><br><br>
      <input type="submit" value="Submit" (click) = "checkCons()">
      <input type="submit" value="Cancel" (click) = "goBack2()">
    </form>
  </div>
  

  
  
  
